The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, 1).

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, 1).


The TRS R consists of the following rules:

f1(a, x) → g1(x, x)
f1(x, a) → g2(x, x)
f2(a, x) → g1(x, x)
f2(x, a) → g2(x, x)
g1(a, x) → h1(x)
g1(x, a) → h2(x)
g2(a, x) → h1(x)
g2(x, a) → h2(x)
h1(a) → i
h2(a) → i
e1(h1(w), h2(w), x, y, z, w) → e2(x, x, y, z, z, w)
e1(x1, x1, x, y, z, a) → e5(x1, x, y, z)
e2(f1(w, w), x, y, z, f2(w, w), w) → e3(x, y, x, y, y, z, y, z, x, y, z, w)
e2(x, x, y, z, z, a) → e6(x, y, z)
e2(i, x, y, z, i, a) → e6(x, y, z)
e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) → e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)
e3(x, y, x, y, y, z, y, z, x, y, z, a) → e6(x, y, z)
e4(g1(w, w), x1, g2(w, w), x1, g1(w, w), x1, g2(w, w), x1, x, y, z, w) → e1(x1, x1, x, y, z, w)
e4(i, x1, i, x1, i, x1, i, x1, x, y, z, a) → e5(x1, x, y, z)
e4(x, x, x, x, x, x, x, x, x, x, x, a) → e6(x, x, x)
e5(i, x, y, z) → e6(x, y, z)

Rewrite Strategy: INNERMOST

(1) NestedDefinedSymbolProof (BOTH BOUNDS(ID, ID) transformation)

The TRS does not nest defined symbols.
Hence, the left-hand sides of the following rules are not basic-reachable and can be removed:
e1(h1(w), h2(w), x, y, z, w) → e2(x, x, y, z, z, w)
e2(f1(w, w), x, y, z, f2(w, w), w) → e3(x, y, x, y, y, z, y, z, x, y, z, w)
e4(g1(w, w), x1, g2(w, w), x1, g1(w, w), x1, g2(w, w), x1, x, y, z, w) → e1(x1, x1, x, y, z, w)

(2) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, 1).


The TRS R consists of the following rules:

e1(x1, x1, x, y, z, a) → e5(x1, x, y, z)
e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) → e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)
g1(a, x) → h1(x)
f1(a, x) → g1(x, x)
f2(a, x) → g1(x, x)
e4(x, x, x, x, x, x, x, x, x, x, x, a) → e6(x, x, x)
e5(i, x, y, z) → e6(x, y, z)
h1(a) → i
e4(i, x1, i, x1, i, x1, i, x1, x, y, z, a) → e5(x1, x, y, z)
h2(a) → i
g2(a, x) → h1(x)
e3(x, y, x, y, y, z, y, z, x, y, z, a) → e6(x, y, z)
e2(i, x, y, z, i, a) → e6(x, y, z)
g2(x, a) → h2(x)
f2(x, a) → g2(x, x)
e2(x, x, y, z, z, a) → e6(x, y, z)
f1(x, a) → g2(x, x)
g1(x, a) → h2(x)

Rewrite Strategy: INNERMOST

(3) TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID) transformation)

Transformed TRS to weighted TRS

(4) Obligation:

The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, 1).


The TRS R consists of the following rules:

e1(x1, x1, x, y, z, a) → e5(x1, x, y, z) [1]
e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) → e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) [1]
g1(a, x) → h1(x) [1]
f1(a, x) → g1(x, x) [1]
f2(a, x) → g1(x, x) [1]
e4(x, x, x, x, x, x, x, x, x, x, x, a) → e6(x, x, x) [1]
e5(i, x, y, z) → e6(x, y, z) [1]
h1(a) → i [1]
e4(i, x1, i, x1, i, x1, i, x1, x, y, z, a) → e5(x1, x, y, z) [1]
h2(a) → i [1]
g2(a, x) → h1(x) [1]
e3(x, y, x, y, y, z, y, z, x, y, z, a) → e6(x, y, z) [1]
e2(i, x, y, z, i, a) → e6(x, y, z) [1]
g2(x, a) → h2(x) [1]
f2(x, a) → g2(x, x) [1]
e2(x, x, y, z, z, a) → e6(x, y, z) [1]
f1(x, a) → g2(x, x) [1]
g1(x, a) → h2(x) [1]

Rewrite Strategy: INNERMOST

(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(6) Obligation:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

e1(x1, x1, x, y, z, a) → e5(x1, x, y, z) [1]
e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) → e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) [1]
g1(a, x) → h1(x) [1]
f1(a, x) → g1(x, x) [1]
f2(a, x) → g1(x, x) [1]
e4(x, x, x, x, x, x, x, x, x, x, x, a) → e6(x, x, x) [1]
e5(i, x, y, z) → e6(x, y, z) [1]
h1(a) → i [1]
e4(i, x1, i, x1, i, x1, i, x1, x, y, z, a) → e5(x1, x, y, z) [1]
h2(a) → i [1]
g2(a, x) → h1(x) [1]
e3(x, y, x, y, y, z, y, z, x, y, z, a) → e6(x, y, z) [1]
e2(i, x, y, z, i, a) → e6(x, y, z) [1]
g2(x, a) → h2(x) [1]
f2(x, a) → g2(x, x) [1]
e2(x, x, y, z, z, a) → e6(x, y, z) [1]
f1(x, a) → g2(x, x) [1]
g1(x, a) → h2(x) [1]

The TRS has the following type information:

e1 :: i → i → i → i → i → a → e6 a :: a e5 :: i → i → i → i → e6 e3 :: i → i → i → i → i → i → i → i → i → i → i → a → e6 e4 :: i → i → i → i → i → i → i → i → i → i → i → a → e6 g1 :: a → a → i h1 :: a → i f1 :: a → a → i f2 :: a → a → i e6 :: i → i → i → e6 i :: i h2 :: a → i g2 :: a → a → i e2 :: i → i → i → i → i → a → e6

Rewrite Strategy: INNERMOST

(7) CompletionProof (UPPER BOUND(ID) transformation)

The TRS is a completely defined constructor system, as every type has a constant constructor and the following rules were added:

e1(v0, v1, v2, v3, v4, v5) → null_e1 [0]
e3(v0, v1, v2, v3, v4, v5, v6, v7, v8, v9, v10, v11) → null_e3 [0]
e4(v0, v1, v2, v3, v4, v5, v6, v7, v8, v9, v10, v11) → null_e4 [0]

And the following fresh constants:

null_e1, null_e3, null_e4

(8) Obligation:

Runtime Complexity Weighted TRS where all functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: e1(x1, x1, x, y, z, a) → e5(x1, x, y, z) [1] e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) → e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) [1] g1(a, x) → h1(x) [1] f1(a, x) → g1(x, x) [1] f2(a, x) → g1(x, x) [1] e4(x, x, x, x, x, x, x, x, x, x, x, a) → e6(x, x, x) [1] e5(i, x, y, z) → e6(x, y, z) [1] h1(a) → i [1] e4(i, x1, i, x1, i, x1, i, x1, x, y, z, a) → e5(x1, x, y, z) [1] h2(a) → i [1] g2(a, x) → h1(x) [1] e3(x, y, x, y, y, z, y, z, x, y, z, a) → e6(x, y, z) [1] e2(i, x, y, z, i, a) → e6(x, y, z) [1] g2(x, a) → h2(x) [1] f2(x, a) → g2(x, x) [1] e2(x, x, y, z, z, a) → e6(x, y, z) [1] f1(x, a) → g2(x, x) [1] g1(x, a) → h2(x) [1] e1(v0, v1, v2, v3, v4, v5) → null_e1 [0] e3(v0, v1, v2, v3, v4, v5, v6, v7, v8, v9, v10, v11) → null_e3 [0] e4(v0, v1, v2, v3, v4, v5, v6, v7, v8, v9, v10, v11) → null_e4 [0] The TRS has the following type information: e1 :: i → i → i → i → i → a → e6:null_e1:null_e3:null_e4 a :: a e5 :: i → i → i → i → e6:null_e1:null_e3:null_e4 e3 :: i → i → i → i → i → i → i → i → i → i → i → a → e6:null_e1:null_e3:null_e4 e4 :: i → i → i → i → i → i → i → i → i → i → i → a → e6:null_e1:null_e3:null_e4 g1 :: a → a → i h1 :: a → i f1 :: a → a → i f2 :: a → a → i e6 :: i → i → i → e6:null_e1:null_e3:null_e4 i :: i h2 :: a → i g2 :: a → a → i e2 :: i → i → i → i → i → a → e6:null_e1:null_e3:null_e4 null_e1 :: e6:null_e1:null_e3:null_e4 null_e3 :: e6:null_e1:null_e3:null_e4 null_e4 :: e6:null_e1:null_e3:null_e4 Rewrite Strategy: INNERMOST

(9) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID) transformation)

Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction.
The constant constructors are abstracted as follows:

a => 0
i => 0
null_e1 => 0
null_e3 => 0
null_e4 => 0

(10) Obligation:

Complexity RNTS consisting of the following rules:

e1(z', z'', z1, z2, z3, z4) -{ 1 }→ e5(x1, x, y, z) :|: z'' = x1, z2 = y, z4 = 0, x1 >= 0, z >= 0, z3 = z, x >= 0, y >= 0, z' = x1, z1 = x
e1(z', z'', z1, z2, z3, z4) -{ 0 }→ 0 :|: z2 = v3, z4 = v5, v0 >= 0, v4 >= 0, z1 = v2, v1 >= 0, v5 >= 0, z'' = v1, z3 = v4, v2 >= 0, v3 >= 0, z' = v0
e2(z', z'', z1, z2, z3, z4) -{ 1 }→ 1 + x + y + z :|: z1 = y, z4 = 0, z >= 0, z2 = z, z3 = 0, x >= 0, y >= 0, z'' = x, z' = 0
e2(z', z'', z1, z2, z3, z4) -{ 1 }→ 1 + x + y + z :|: z1 = y, z4 = 0, z >= 0, z' = x, z2 = z, z3 = z, x >= 0, y >= 0, z'' = x
e3(z', z'', z1, z2, z3, z4, z5, z6, z7, z8, z9, z10) -{ 1 }→ e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) :|: z5 = x4, z7 = x, z1 = x2, y >= 0, z' = x1, z2 = x2, w >= 0, z3 = x3, z4 = x3, x2 >= 0, x3 >= 0, z'' = x1, z9 = z, x1 >= 0, x4 >= 0, z >= 0, z10 = w, x >= 0, z6 = x4, z8 = y
e3(z', z'', z1, z2, z3, z4, z5, z6, z7, z8, z9, z10) -{ 0 }→ 0 :|: z4 = v5, v0 >= 0, v8 >= 0, z8 = v9, z9 = v10, v6 >= 0, v1 >= 0, v5 >= 0, z'' = v1, z3 = v4, v2 >= 0, v3 >= 0, z' = v0, z10 = v11, v11 >= 0, z2 = v3, v4 >= 0, z5 = v6, z1 = v2, v7 >= 0, v9 >= 0, v10 >= 0, z6 = v7, z7 = v8
e3(z', z'', z1, z2, z3, z4, z5, z6, z7, z8, z9, z10) -{ 1 }→ 1 + x + y + z :|: z7 = x, z' = x, z'' = y, z3 = y, y >= 0, z1 = x, z2 = y, z4 = z, z5 = y, z9 = z, z >= 0, x >= 0, z6 = z, z8 = y, z10 = 0
e4(z', z'', z1, z2, z3, z4, z5, z6, z7, z8, z9, z10) -{ 1 }→ e5(x1, x, y, z) :|: z5 = 0, z7 = x, z2 = x1, z3 = 0, y >= 0, z6 = x1, z' = 0, z'' = x1, z1 = 0, z4 = x1, z9 = z, x1 >= 0, z >= 0, x >= 0, z8 = y, z10 = 0
e4(z', z'', z1, z2, z3, z4, z5, z6, z7, z8, z9, z10) -{ 0 }→ 0 :|: z4 = v5, v0 >= 0, v8 >= 0, z8 = v9, z9 = v10, v6 >= 0, v1 >= 0, v5 >= 0, z'' = v1, z3 = v4, v2 >= 0, v3 >= 0, z' = v0, z10 = v11, v11 >= 0, z2 = v3, v4 >= 0, z5 = v6, z1 = v2, v7 >= 0, v9 >= 0, v10 >= 0, z6 = v7, z7 = v8
e4(z', z'', z1, z2, z3, z4, z5, z6, z7, z8, z9, z10) -{ 1 }→ 1 + x + x + x :|: z2 = x, z7 = x, z' = x, z4 = x, z5 = x, z1 = x, z3 = x, z6 = x, x >= 0, z'' = x, z8 = x, z9 = x, z10 = 0
e5(z', z'', z1, z2) -{ 1 }→ 1 + x + y + z :|: z1 = y, z >= 0, z2 = z, x >= 0, y >= 0, z'' = x, z' = 0
f1(z', z'') -{ 1 }→ g2(x, x) :|: z'' = 0, z' = x, x >= 0
f1(z', z'') -{ 1 }→ g1(x, x) :|: x >= 0, z'' = x, z' = 0
f2(z', z'') -{ 1 }→ g2(x, x) :|: z'' = 0, z' = x, x >= 0
f2(z', z'') -{ 1 }→ g1(x, x) :|: x >= 0, z'' = x, z' = 0
g1(z', z'') -{ 1 }→ h2(x) :|: z'' = 0, z' = x, x >= 0
g1(z', z'') -{ 1 }→ h1(x) :|: x >= 0, z'' = x, z' = 0
g2(z', z'') -{ 1 }→ h2(x) :|: z'' = 0, z' = x, x >= 0
g2(z', z'') -{ 1 }→ h1(x) :|: x >= 0, z'' = x, z' = 0
h1(z') -{ 1 }→ 0 :|: z' = 0
h2(z') -{ 1 }→ 0 :|: z' = 0

Only complete derivations are relevant for the runtime complexity.

(11) CompleteCoflocoProof (EQUIVALENT transformation)

Transformed the RNTS (where only complete derivations are relevant) into cost relations for CoFloCo:

eq(start(V, V1, V2, V3, V4, V5, V10, V11, V12, V13, V14, V15),0,[e1(V, V1, V2, V3, V4, V5, Out)],[V >= 0,V1 >= 0,V2 >= 0,V3 >= 0,V4 >= 0,V5 >= 0]). eq(start(V, V1, V2, V3, V4, V5, V10, V11, V12, V13, V14, V15),0,[e3(V, V1, V2, V3, V4, V5, V10, V11, V12, V13, V14, V15, Out)],[V >= 0,V1 >= 0,V2 >= 0,V3 >= 0,V4 >= 0,V5 >= 0,V10 >= 0,V11 >= 0,V12 >= 0,V13 >= 0,V14 >= 0,V15 >= 0]). eq(start(V, V1, V2, V3, V4, V5, V10, V11, V12, V13, V14, V15),0,[g1(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V2, V3, V4, V5, V10, V11, V12, V13, V14, V15),0,[f1(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V2, V3, V4, V5, V10, V11, V12, V13, V14, V15),0,[f2(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V2, V3, V4, V5, V10, V11, V12, V13, V14, V15),0,[e4(V, V1, V2, V3, V4, V5, V10, V11, V12, V13, V14, V15, Out)],[V >= 0,V1 >= 0,V2 >= 0,V3 >= 0,V4 >= 0,V5 >= 0,V10 >= 0,V11 >= 0,V12 >= 0,V13 >= 0,V14 >= 0,V15 >= 0]). eq(start(V, V1, V2, V3, V4, V5, V10, V11, V12, V13, V14, V15),0,[e5(V, V1, V2, V3, Out)],[V >= 0,V1 >= 0,V2 >= 0,V3 >= 0]). eq(start(V, V1, V2, V3, V4, V5, V10, V11, V12, V13, V14, V15),0,[h1(V, Out)],[V >= 0]). eq(start(V, V1, V2, V3, V4, V5, V10, V11, V12, V13, V14, V15),0,[h2(V, Out)],[V >= 0]). eq(start(V, V1, V2, V3, V4, V5, V10, V11, V12, V13, V14, V15),0,[g2(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V2, V3, V4, V5, V10, V11, V12, V13, V14, V15),0,[e2(V, V1, V2, V3, V4, V5, Out)],[V >= 0,V1 >= 0,V2 >= 0,V3 >= 0,V4 >= 0,V5 >= 0]). eq(e1(V, V1, V2, V3, V4, V5, Out),1,[e5(V6, V7, V8, V9, Ret)],[Out = Ret,V1 = V6,V3 = V8,V5 = 0,V6 >= 0,V9 >= 0,V4 = V9,V7 >= 0,V8 >= 0,V = V6,V2 = V7]). eq(e3(V, V1, V2, V3, V4, V5, V10, V11, V12, V13, V14, V15, Out),1,[e4(V16, V16, V17, V17, V18, V18, V19, V19, V20, V21, V22, V23, Ret1)],[Out = Ret1,V10 = V19,V12 = V20,V2 = V17,V21 >= 0,V = V16,V3 = V17,V23 >= 0,V4 = V18,V5 = V18,V17 >= 0,V18 >= 0,V1 = V16,V14 = V22,V16 >= 0,V19 >= 0,V22 >= 0,V15 = V23,V20 >= 0,V11 = V19,V13 = V21]). eq(g1(V, V1, Out),1,[h1(V24, Ret2)],[Out = Ret2,V24 >= 0,V1 = V24,V = 0]). eq(f1(V, V1, Out),1,[g1(V25, V25, Ret3)],[Out = Ret3,V25 >= 0,V1 = V25,V = 0]). eq(f2(V, V1, Out),1,[g1(V26, V26, Ret4)],[Out = Ret4,V26 >= 0,V1 = V26,V = 0]). eq(e4(V, V1, V2, V3, V4, V5, V10, V11, V12, V13, V14, V15, Out),1,[],[Out = 1 + 3*V27,V3 = V27,V12 = V27,V = V27,V5 = V27,V10 = V27,V2 = V27,V4 = V27,V11 = V27,V27 >= 0,V1 = V27,V13 = V27,V14 = V27,V15 = 0]). eq(e5(V, V1, V2, V3, Out),1,[],[Out = 1 + V28 + V29 + V30,V2 = V29,V30 >= 0,V3 = V30,V28 >= 0,V29 >= 0,V1 = V28,V = 0]). eq(h1(V, Out),1,[],[Out = 0,V = 0]). eq(e4(V, V1, V2, V3, V4, V5, V10, V11, V12, V13, V14, V15, Out),1,[e5(V31, V32, V33, V34, Ret5)],[Out = Ret5,V10 = 0,V12 = V32,V3 = V31,V4 = 0,V33 >= 0,V11 = V31,V = 0,V1 = V31,V2 = 0,V5 = V31,V14 = V34,V31 >= 0,V34 >= 0,V32 >= 0,V13 = V33,V15 = 0]). eq(h2(V, Out),1,[],[Out = 0,V = 0]). eq(g2(V, V1, Out),1,[h1(V35, Ret6)],[Out = Ret6,V35 >= 0,V1 = V35,V = 0]). eq(e3(V, V1, V2, V3, V4, V5, V10, V11, V12, V13, V14, V15, Out),1,[],[Out = 1 + V36 + V37 + V38,V12 = V36,V = V36,V1 = V37,V4 = V37,V37 >= 0,V2 = V36,V3 = V37,V5 = V38,V10 = V37,V14 = V38,V38 >= 0,V36 >= 0,V11 = V38,V13 = V37,V15 = 0]). eq(e2(V, V1, V2, V3, V4, V5, Out),1,[],[Out = 1 + V39 + V40 + V41,V2 = V40,V5 = 0,V41 >= 0,V3 = V41,V4 = 0,V39 >= 0,V40 >= 0,V1 = V39,V = 0]). eq(g2(V, V1, Out),1,[h2(V42, Ret7)],[Out = Ret7,V1 = 0,V = V42,V42 >= 0]). eq(f2(V, V1, Out),1,[g2(V43, V43, Ret8)],[Out = Ret8,V1 = 0,V = V43,V43 >= 0]). eq(e2(V, V1, V2, V3, V4, V5, Out),1,[],[Out = 1 + V44 + V45 + V46,V2 = V45,V5 = 0,V46 >= 0,V = V44,V3 = V46,V4 = V46,V44 >= 0,V45 >= 0,V1 = V44]). eq(f1(V, V1, Out),1,[g2(V47, V47, Ret9)],[Out = Ret9,V1 = 0,V = V47,V47 >= 0]). eq(g1(V, V1, Out),1,[h2(V48, Ret10)],[Out = Ret10,V1 = 0,V = V48,V48 >= 0]). eq(e1(V, V1, V2, V3, V4, V5, Out),0,[],[Out = 0,V3 = V49,V5 = V50,V51 >= 0,V52 >= 0,V2 = V53,V54 >= 0,V50 >= 0,V1 = V54,V4 = V52,V53 >= 0,V49 >= 0,V = V51]). eq(e3(V, V1, V2, V3, V4, V5, V10, V11, V12, V13, V14, V15, Out),0,[],[Out = 0,V5 = V55,V56 >= 0,V57 >= 0,V13 = V58,V14 = V59,V60 >= 0,V61 >= 0,V55 >= 0,V1 = V61,V4 = V62,V63 >= 0,V64 >= 0,V = V56,V15 = V65,V65 >= 0,V3 = V64,V62 >= 0,V10 = V60,V2 = V63,V66 >= 0,V58 >= 0,V59 >= 0,V11 = V66,V12 = V57]). eq(e4(V, V1, V2, V3, V4, V5, V10, V11, V12, V13, V14, V15, Out),0,[],[Out = 0,V5 = V67,V68 >= 0,V69 >= 0,V13 = V70,V14 = V71,V72 >= 0,V73 >= 0,V67 >= 0,V1 = V73,V4 = V74,V75 >= 0,V76 >= 0,V = V68,V15 = V77,V77 >= 0,V3 = V76,V74 >= 0,V10 = V72,V2 = V75,V78 >= 0,V70 >= 0,V71 >= 0,V11 = V78,V12 = V69]). input_output_vars(e1(V,V1,V2,V3,V4,V5,Out),[V,V1,V2,V3,V4,V5],[Out]). input_output_vars(e3(V,V1,V2,V3,V4,V5,V10,V11,V12,V13,V14,V15,Out),[V,V1,V2,V3,V4,V5,V10,V11,V12,V13,V14,V15],[Out]). input_output_vars(g1(V,V1,Out),[V,V1],[Out]). input_output_vars(f1(V,V1,Out),[V,V1],[Out]). input_output_vars(f2(V,V1,Out),[V,V1],[Out]). input_output_vars(e4(V,V1,V2,V3,V4,V5,V10,V11,V12,V13,V14,V15,Out),[V,V1,V2,V3,V4,V5,V10,V11,V12,V13,V14,V15],[Out]). input_output_vars(e5(V,V1,V2,V3,Out),[V,V1,V2,V3],[Out]). input_output_vars(h1(V,Out),[V],[Out]). input_output_vars(h2(V,Out),[V],[Out]). input_output_vars(g2(V,V1,Out),[V,V1],[Out]). input_output_vars(e2(V,V1,V2,V3,V4,V5,Out),[V,V1,V2,V3,V4,V5],[Out]).

CoFloCo proof output:
Preprocessing Cost Relations
=====================================

#### Computed strongly connected components
0. non_recursive : [e5/5]
1. non_recursive : [e1/7]
2. non_recursive : [e2/7]
3. non_recursive : [e4/13]
4. non_recursive : [e3/13]
5. non_recursive : [h1/2]
6. non_recursive : [h2/2]
7. non_recursive : [g1/3]
8. non_recursive : [g2/3]
9. non_recursive : [f1/3]
10. non_recursive : [f2/3]
11. non_recursive : [start/12]

#### Obtained direct recursion through partial evaluation
0. SCC is completely evaluated into other SCCs
1. SCC is partially evaluated into e1/7
2. SCC is partially evaluated into e2/7
3. SCC is partially evaluated into e4/13
4. SCC is partially evaluated into e3/13
5. SCC is completely evaluated into other SCCs
6. SCC is completely evaluated into other SCCs
7. SCC is partially evaluated into g1/3
8. SCC is partially evaluated into g2/3
9. SCC is partially evaluated into f1/3
10. SCC is partially evaluated into f2/3
11. SCC is partially evaluated into start/12

Control-Flow Refinement of Cost Relations
=====================================

### Specialization of cost equations e1/7
* CE 12 is refined into CE [27]
* CE 11 is refined into CE [28]


### Cost equations --> "Loop" of e1/7
* CEs [27] --> Loop 19
* CEs [28] --> Loop 20

### Ranking functions of CR e1(V,V1,V2,V3,V4,V5,Out)

#### Partial ranking functions of CR e1(V,V1,V2,V3,V4,V5,Out)


### Specialization of cost equations e2/7
* CE 26 is refined into CE [29]
* CE 25 is refined into CE [30]


### Cost equations --> "Loop" of e2/7
* CEs [29] --> Loop 21
* CEs [30] --> Loop 22

### Ranking functions of CR e2(V,V1,V2,V3,V4,V5,Out)

#### Partial ranking functions of CR e2(V,V1,V2,V3,V4,V5,Out)


### Specialization of cost equations e4/13
* CE 23 is refined into CE [31]
* CE 21 is refined into CE [32]
* CE 22 is refined into CE [33]


### Cost equations --> "Loop" of e4/13
* CEs [31] --> Loop 23
* CEs [32] --> Loop 24
* CEs [33] --> Loop 25

### Ranking functions of CR e4(V,V1,V2,V3,V4,V5,V10,V11,V12,V13,V14,V15,Out)

#### Partial ranking functions of CR e4(V,V1,V2,V3,V4,V5,V10,V11,V12,V13,V14,V15,Out)


### Specialization of cost equations e3/13
* CE 13 is refined into CE [34,35,36]
* CE 15 is refined into CE [37]
* CE 14 is refined into CE [38]


### Cost equations --> "Loop" of e3/13
* CEs [36,37] --> Loop 26
* CEs [35,38] --> Loop 27
* CEs [34] --> Loop 28

### Ranking functions of CR e3(V,V1,V2,V3,V4,V5,V10,V11,V12,V13,V14,V15,Out)

#### Partial ranking functions of CR e3(V,V1,V2,V3,V4,V5,V10,V11,V12,V13,V14,V15,Out)


### Specialization of cost equations g1/3
* CE 16 is refined into CE [39]


### Cost equations --> "Loop" of g1/3
* CEs [39] --> Loop 29

### Ranking functions of CR g1(V,V1,Out)

#### Partial ranking functions of CR g1(V,V1,Out)


### Specialization of cost equations g2/3
* CE 24 is refined into CE [40]


### Cost equations --> "Loop" of g2/3
* CEs [40] --> Loop 30

### Ranking functions of CR g2(V,V1,Out)

#### Partial ranking functions of CR g2(V,V1,Out)


### Specialization of cost equations f1/3
* CE 18 is refined into CE [41]
* CE 17 is refined into CE [42]


### Cost equations --> "Loop" of f1/3
* CEs [41,42] --> Loop 31

### Ranking functions of CR f1(V,V1,Out)

#### Partial ranking functions of CR f1(V,V1,Out)


### Specialization of cost equations f2/3
* CE 20 is refined into CE [43]
* CE 19 is refined into CE [44]


### Cost equations --> "Loop" of f2/3
* CEs [43,44] --> Loop 32

### Ranking functions of CR f2(V,V1,Out)

#### Partial ranking functions of CR f2(V,V1,Out)


### Specialization of cost equations start/12
* CE 2 is refined into CE [45,46]
* CE 3 is refined into CE [47,48,49]
* CE 4 is refined into CE [50]
* CE 5 is refined into CE [51]
* CE 6 is refined into CE [52]
* CE 7 is refined into CE [53,54,55]
* CE 9 is refined into CE [56]
* CE 10 is refined into CE [57,58]
* CE 8 is refined into CE [59]


### Cost equations --> "Loop" of start/12
* CEs [48,54] --> Loop 33
* CEs [46,49,55,58] --> Loop 34
* CEs [45,47,50,51,52,53,56,57,59] --> Loop 35

### Ranking functions of CR start(V,V1,V2,V3,V4,V5,V10,V11,V12,V13,V14,V15)

#### Partial ranking functions of CR start(V,V1,V2,V3,V4,V5,V10,V11,V12,V13,V14,V15)


Computing Bounds
=====================================

#### Cost of chains of e1(V,V1,V2,V3,V4,V5,Out):
* Chain [20]: 2
with precondition: [V=0,V1=0,V5=0,V2+V3+V4+1=Out,V2>=0,V3>=0,V4>=0]

* Chain [19]: 0
with precondition: [Out=0,V>=0,V1>=0,V2>=0,V3>=0,V4>=0,V5>=0]


#### Cost of chains of e2(V,V1,V2,V3,V4,V5,Out):
* Chain [22]: 1
with precondition: [V=0,V4=0,V5=0,V1+V2+V3+1=Out,V1>=0,V2>=0,V3>=0]

* Chain [21]: 1
with precondition: [V5=0,V=V1,V3=V4,V+V2+V3+1=Out,V>=0,V2>=0,V3>=0]


#### Cost of chains of e4(V,V1,V2,V3,V4,V5,V10,V11,V12,V13,V14,V15,Out):
* Chain [25]: 2
with precondition: [V=0,V1=0,V2=0,V3=0,V4=0,V5=0,V10=0,V11=0,V15=0,V12+V13+V14+1=Out,V12>=0,V13>=0,V14>=0]

* Chain [24]: 1
with precondition: [V15=0,V=V1,V=V2,V=V3,V=V4,V=V5,V=V10,V=V11,V=V12,V=V13,V=V14,3*V+1=Out,V>=0]

* Chain [23]: 0
with precondition: [Out=0,V>=0,V1>=0,V2>=0,V3>=0,V4>=0,V5>=0,V10>=0,V11>=0,V12>=0,V13>=0,V14>=0,V15>=0]


#### Cost of chains of e3(V,V1,V2,V3,V4,V5,V10,V11,V12,V13,V14,V15,Out):
* Chain [28]: 3
with precondition: [V=0,V1=0,V2=0,V3=0,V4=0,V5=0,V10=0,V11=0,V15=0,V12+V13+V14+1=Out,V12>=0,V13>=0,V14>=0]

* Chain [27]: 2
with precondition: [V15=0,V=V2,V1=V3,V1=V4,V1=V10,V5=V11,V=V12,V1=V13,V5=V14,V+V1+V5+1=Out,V>=0,V1>=0,V5>=0]

* Chain [26]: 1
with precondition: [Out=0,V>=0,V1>=0,V2>=0,V3>=0,V4>=0,V5>=0,V10>=0,V11>=0,V12>=0,V13>=0,V14>=0,V15>=0]


#### Cost of chains of g1(V,V1,Out):
* Chain [29]: 2
with precondition: [V=0,V1=0,Out=0]


#### Cost of chains of g2(V,V1,Out):
* Chain [30]: 2
with precondition: [V=0,V1=0,Out=0]


#### Cost of chains of f1(V,V1,Out):
* Chain [31]: 3
with precondition: [V=0,V1=0,Out=0]


#### Cost of chains of f2(V,V1,Out):
* Chain [32]: 3
with precondition: [V=0,V1=0,Out=0]


#### Cost of chains of start(V,V1,V2,V3,V4,V5,V10,V11,V12,V13,V14,V15):
* Chain [35]: 3
with precondition: [V=0]

* Chain [34]: 1
with precondition: [V>=0,V1>=0,V2>=0,V3>=0,V4>=0,V5>=0]

* Chain [33]: 2
with precondition: [V15=0,V=V2,V1=V3,V1=V4,V1=V10,V5=V11,V=V12,V1=V13,V5=V14,V>=0,V1>=0,V5>=0]


Closed-form bounds of start(V,V1,V2,V3,V4,V5,V10,V11,V12,V13,V14,V15):
-------------------------------------
* Chain [35] with precondition: [V=0]
- Upper bound: 3
- Complexity: constant
* Chain [34] with precondition: [V>=0,V1>=0,V2>=0,V3>=0,V4>=0,V5>=0]
- Upper bound: 1
- Complexity: constant
* Chain [33] with precondition: [V15=0,V=V2,V1=V3,V1=V4,V1=V10,V5=V11,V=V12,V1=V13,V5=V14,V>=0,V1>=0,V5>=0]
- Upper bound: 2
- Complexity: constant

### Maximum cost of start(V,V1,V2,V3,V4,V5,V10,V11,V12,V13,V14,V15): 3
Asymptotic class: constant
* Total analysis performed in 423 ms.

(12) BOUNDS(1, 1)